Nuprl Lemma : bool-to-dcdr_wf
11,40
postcript
pdf
A
:Type,
f
:(
A
),
x
:
A
. {
f
}
(
x
)
Dec(
f
(
x
) = tt)
latex
ProofTree
Definitions
Type
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
s
=
t
,
,
t
T
,
f
(
a
)
,
{
f
}
,
tt
origin
A:Type, f:(A
), x:A. {f}
(x) 
Dec(f(x) = tt)
A:Type, f:(A), x:A. {f}(x) Dec(f(x) = tt)
B(x)x:A. B(x) T